#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)

/* Toutes les obligations de preuve sont validées */

/*@ predicate isMin (int *a, integer n,integer x) = 
  @   \forall integer k;(0<=k<n) ==> (a[k] >= a[x]);
  @*/

/*@ predicate isLast (int *a, integer n, integer x) =
  @   \forall integer k; x<k<n ==> a[k]!=a[x];
  @*/


/*@ 
  @ requires \valid_range(a,0,n-1);
  @ requires n > 0;
  @ ensures 0<=\result<n;
  @ ensures isMin(a,n,\result);
  @ ensures isLast(a,n,\result);
  @*/
int arrayminlast(int * a, int n) {
  int i = 0, imin = i;
  /*@
    @ loop invariant 0<=imin<n && 0<=i<=n;
    @ loop invariant isMin(a,i,imin);
    @ loop invariant isLast(a,i,imin);
    @ loop variant n-i;
    @*/
  while (i < n) {
    imin = (a[i] <= a[imin] ? i : imin);
    ++i;
  }
  return imin;
}
